Problem:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
Proof:
Complexity Transformation Processor:
strict:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0) = x0 + 32,
[a](x0) = x0 + 1,
[f](x0, x1) = x0 + x1 + 127,
[s](x0) = x0 + 1
orientation:
f(s(X),X) = 2X + 128 >= 2X + 128 = f(X,a(X))
f(X,c(X)) = 2X + 159 >= 2X + 128 = f(s(X),X)
f(X,X) = 2X + 127 >= X + 32 = c(X)
problem:
strict:
f(s(X),X) -> f(X,a(X))
weak:
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0) = x0 + 96,
[a](x0) = x0 + 64,
[f](x0, x1) = x0 + x1 + 96,
[s](x0) = x0 + 96
orientation:
f(s(X),X) = 2X + 192 >= 2X + 160 = f(X,a(X))
f(X,c(X)) = 2X + 192 >= 2X + 192 = f(s(X),X)
f(X,X) = 2X + 96 >= X + 96 = c(X)
problem:
strict:
weak:
f(s(X),X) -> f(X,a(X))
f(X,c(X)) -> f(s(X),X)
f(X,X) -> c(X)
Qed